Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
ap(ap(g,x),y) |
→ y |
| 2: |
|
ap(f,x) |
→ ap(f,app(g,x)) |
|
There is one dependency pair:
|
| 3: |
|
AP(f,x) |
→ AP(f,app(g,x)) |
|
The approximated dependency graph contains one SCC:
{3}.
-
Consider the SCC {3}.
There are no usable rules.
The constraints could not be solved.
Tyrolean Termination Tool (0.00 seconds)
--- May 3, 2006